es:ES, l:IdLnk, tg:Id, e:E.
kind(e) = rcv(l,tg)  Knd
 {isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l)  Id} 

latex

Definitions	2of(t), SQType(T), (Msg on l), {i..j}, ||as||, sends(l;e), index(e), locl(a), 1of(t), T, A, Dec(P), P  Q, loc(e), sender(e), source(l), False, isrcv(k), lnk(k), tag(k), True, P  Q, Prop, Knd, kind(e), rcv(l,tg), E, x:A. B(x), t  T, ES, isrcv(e), lnk(e), tag(e), {T}, A & B, P & Q, Id, IdLnk, b
Lemmas	event system wf, IdLnk wf, Id wf, es-E wf, rcv wf, es-kind wf, Knd wf, false wf, true wf, lsrc wf, es-sender wf, es-loc wf, decidable equal Id, es-lnk wf, es-axioms, squash wf, not wf, not rcv locl, es-index wf, length wf2, es-Msgl wf, length wf1, guard wf